/*
Copyright 2007 Laura Giordano, Valentina Gliozzi, Gian Luca Pozzato

    This file is part of KLMLean.

    KLMLean is free software: you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation, either version 3 of the License, or
    (at your option) any later version.

    KLMLean is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with KLMLean.  If not, see <http://www.gnu.org/licenses/>.
*/


/* Theorem prover for KLM Loop cumulative logic CL */
:- op(400,fy,neg), 
   op(400,fy,box),
   op(400,fy,l),
   op(500,xfy,and), 
   op(600,xfy,or),
   op(650,xfy,->), 
   op(650,xfy,=>).
:-use_module(library(lists)).


/* --------------------------------------------------------------------------------------- */

/* The following predicate implements the calculi:

    prove(Gamma,[],Tree) iff there exists a closed tableaux Tree for Gamma;\emptyset
    
*/

prove([],_,_):-!,fail.

prove(Gamma,_,tree(ax,F)):-member(neg F,Gamma),member(F, Gamma),!.

prove(Gamma,Sigma,tree(andP,F,G,ST)):-select(F and G,Gamma,NewGamma),!,
                                      prove([F|[G|NewGamma]],Sigma,ST).

prove(Gamma,Sigma,tree(orN,F,G,ST)):-select(neg (F or G),Gamma,NewGamma),!,
                                     prove([neg F|[neg G|NewGamma]],Sigma,ST).


prove(Gamma,Sigma,tree(impN,F,G,ST)):-select(neg (F -> G),Gamma,NewGamma),!,
                                     prove([F|[neg G|NewGamma]],Sigma,ST).

prove(Gamma,Sigma,tree(neg,F,ST)):-select(neg neg F,Gamma,NewGamma),!,              
                           prove([F|NewGamma],Sigma,ST).

prove(Gamma,Sigma,tree(andN,F,G,ST1,ST2)):-select(neg (F and G),Gamma,NewGamma),!,
                                      prove([neg F|NewGamma],Sigma,ST1),!,
                                      prove([neg G|NewGamma],Sigma,ST2).

prove(Gamma,Sigma,tree(orP,F,G,ST1,ST2)):-select(F or G,Gamma,NewGamma),!,
                                      prove([F|NewGamma],Sigma,ST1),!,
                                      prove([G|NewGamma],Sigma,ST2).
     
prove(Gamma,Sigma,tree(impP,F,G,ST1,ST2)):-select(F -> G,Gamma,NewGamma),!,
                                       prove([neg F|NewGamma],Sigma,ST1),!,
                                       prove([G|NewGamma],Sigma,ST2).
                

                                       
prove(Gamma,Sigma,tree(entN,A,B,ST)):-select(neg (A => B),Gamma,NewGamma),
                                      conditionals(NewGamma,CondGamma),                                  
                                      append(Sigma,CondGamma,DefGamma),
                                      prove([l A|[box neg l A|[neg l B|DefGamma]]],[],ST).
            

prove(Gamma,_,tree(elleN,A,ST)):-select(neg l A,Gamma,NewGamma),
                                     inelle(NewGamma,DefGamma),
                                     prove([neg A|DefGamma],[],ST).                                       

prove(Gamma,_,tree(elleN,ST)):-inelle(Gamma,DefGamma),
                                   prove(DefGamma,[],ST).                                       


prove(Gamma,Sigma,tree(boxN,A,ST)):-select(neg box neg l A,Gamma,NewGamma),
                            conditionals(NewGamma,CondGamma),
                            boxed(NewGamma,Boxed),
                            inboxed(Boxed,Inboxed),
                            append(Sigma,Boxed,Temp1),
                            append(Inboxed,CondGamma,Temp2),
                            append(Temp1,Temp2,DefGamma),
                            prove([l A|[box neg l A|DefGamma]],[],ST).
   

/* Remark: as a difference from the rule (|~+) presented in the papers, having 3 conclusions,  
   KLMLean 2.0 implements an equivalent one having only two conclusions: 
   
        \Gamma, A |~ B 				\Gamma, A |~ B
    -----------------------------	  ------------------------------
      (1) \Gamma, A |~ B, ~LA	            (1) \Gamma, A |~ B, LA -> LB
      (2) \Gamma, A |~ B, ~[]~LA	    (2) \Gamma, A |~ B, ~[]~LA
      (3) \Gamma, A |~ B, LB

   This chioce has been made in order to simplify the graphical user interface, displaying 
   only binary trees.

*/   
prove(Gamma,Sigma,tree(entP,A,B,ST1,ST2)):-select(A => B,Gamma,NewGamma),!,
                                       prove([neg box neg l A|NewGamma],[A => B|Sigma],ST1),!,
                                       prove([l A -> l B|NewGamma],[A => B|Sigma],ST2).        
                                       
/* Auxiliary predicates */

inelle([],[]):-!.
inelle([l A|Tail],[A|ResTail]):-!,inelle(Tail,ResTail).
inelle([_|Tail],ResTail):-!,inelle(Tail,ResTail).

conditionals([],[]):-!.
conditionals([A => B|Tail],[A => B|CondTail]):-!,conditionals(Tail,CondTail).
conditionals([neg (A => B)|Tail],[neg (A => B)|CondTail]):-!,conditionals(Tail,CondTail).
conditionals([_|Tail],CondTail):-conditionals(Tail,CondTail).

boxed([],[]):-!.
boxed([box A|Tail],[box A|BoxTail]):-!,boxed(Tail,BoxTail).
boxed([_|Tail],BoxTail):-boxed(Tail,BoxTail).
        
inboxed([],[]):-!.
inboxed([box A|Tail],[A|InBoxTail]):-!,inboxed(Tail,InBoxTail).
inboxed([_|Tail],InBoxTail):-inboxed(Tail,InBoxTail).


/* Predicate used to control that the inserted formula belongs to the language LCL of CL logic:

  - propositional formulas belong to LCL
  - if A and B are propositionals, then A => B belongs to LCL
  - a boolean combination F of formulas of LCL belongs to LCL
  
*/

parseinput([]):-!.
parseinput([F|Tail]):-parse(F),parseinput(Tail).

parse(P):-atom(P).
parse(F and G):-parse(F),parse(G).
parse(F or G):-parse(F),parse(G).
parse(F -> G):-parse(F),parse(G).
parse(neg F):-parse(F).
parse(A => B):-boolcomb(A),boolcomb(B).

boolcomb(P):-atom(P).
boolcomb(A and B):-boolcomb(A),boolcomb(B).
boolcomb(A or B):-boolcomb(A),boolcomb(B).
boolcomb(A -> B):-boolcomb(A),boolcomb(B).
boolcomb(neg A):-boolcomb(A).


/* Predicates used to reconstruct the proof tree (used by the GUI) */
javaTree(tree(ax,_),Node,jT(ax,Node,null,null)):-!.

javaTree(tree(andP,A,B,Sub),Node,jT(andP,Node,SubJava,null)):-!,
  select(A and B,Node,Temp),
  javaTree(Sub,[A|[B|Temp]],SubJava).
  
javaTree(tree(andN,A,B,S1,S2),Node,jT(andN,Node,SJ1,SJ2)):-!,
  select(neg (A and B),Node,Temp),
  javaTree(S1,[neg A|Temp],SJ1),
  javaTree(S2,[neg B|Temp],SJ2).  
  
javaTree(tree(orP,A,B,S1,S2),Node,jT(orP,Node,SJ1,SJ2)):-!,
  select(A or B,Node,Temp),
  javaTree(S1,[A|Temp],SJ1),  
  javaTree(S2,[B|Temp],SJ2).
  
javaTree(tree(orN,A,B,Sub),Node,jT(orN,Node,SubJava,null)):-!, 
  select(neg (A or B),Node,Temp), 
  javaTree(Sub,[neg A|[neg B|Temp]],SubJava).
  
javaTree(tree(impP,A,B,S1,S2),Node,jT(impP,Node,SJ1,SJ2)):-!,
  select(A -> B,Node,Temp),
  javaTree(S1,[neg A|Temp],SJ1),
  javaTree(S2,[B|Temp],SJ2).
 
javaTree(tree(neg,A,Sub),Node,jT(neg,Node,SubJava,null)):-!,
  select(neg neg A,Node,Temp),
  javaTree(Sub,[A|Temp],SubJava).

javaTree(tree(impN,A,B,Sub),Node,jT(impN,Node,SubJava,null)):-!,   
  select(neg (A -> B),Node,Temp),
  javaTree(Sub,[A|[neg B|Temp]],SubJava).
  
javaTree(tree(entP,A,B,S1,S2),Node,jT(entP,Node,SJ1,SJ2)):-!,
  javaTree(S1,[neg box neg l A|Node],SJ1),  
  javaTree(S2,[l A -> l B|Node],SJ2).
  
javaTree(tree(entN,A,B,Sub),Node,jT(entN,Node,SubJava,null)):-!,  
  select(neg (A => B),Node,Temp),
  conditionals(Temp,Cond),
  javaTree(Sub,[l A|[box neg l A|[neg l B|Cond]]],SubJava).  
  
javaTree(tree(boxN,A,Sub),Node,jT(boxN,Node,SubJava,null)):-!,
  select(neg box neg l A,Node,Temp),
  conditionals(Temp,Cond),
  boxed(Temp,Boxed),
  inboxed(Temp,Inboxed),
  append(Cond,Boxed,T),
  append(T,Inboxed,Def),
  javaTree(Sub,[l A|[box neg l A|Def]],SubJava).

javaTree(tree(elleN,A,Sub),Node,jT(elleN,Node,SubJava,null)):-!,
  select(neg l A,Node,Temp),
  inelle(Temp,Def),
  javaTree(Sub,[neg A|Def],SubJava).
  
javaTree(tree(elleN,Sub),Node,jT(elleN,Node,SubJava,null)):-!,  
  inelle(Node,Temp),
  javaTree(Sub,Temp,SubJava).
                                     

/* Predicates used by the GUI to extract information about the closed tree */

getRule(jT(Rule,_,_,_),Rule):-!.
getNode(jT(_,Node,_,_),Node):-!.
getLeft(jT(_,_,Left,_),Left):-!.
getRight(jT(_,_,_,Right),Right):-!.


/* Top-level predicates */
unsat(Gamma,Tree):-parseinput(Gamma),prove(Gamma,[],Tree).
nmcr(K,F,Tree):-parseinput([F|K]),prove([neg F|K],[],Tree).
unsatinterface(K,[F],Tree):-prove([neg F|K],[],Tree).
unsatinterface(K,[],Tree):-prove(K,[],Tree).